EventsWithValues
== E:Type
==  (eq:EqDecider(E)
==  pred?:(E(?E))
==  info:(E((:Id  Id) + (:(:IdLnk  E)  Id)))
==  oaxioms:EOrderAxioms(E; pred?; info)
==  T:(IdIdType)
==  when:(x:Ide:ET(loc(e),x))
==  after:(x:Ide:ET(loc(e),x))
==  saxiom:(e:E. ((first(e)))  (x:Id. when(x,e) = after(x,pred(e))))
==  V:(KndIdType)
==  (val:(e:EV(kind(e),loc(e)))
==  Top)) 

latex

---

clarification:

EventsWithValues{i}
== E:Type{i}
==  (eq:EqDecider(E)
==  pred?:(E(E + Unit))
==  info:(E((:Id  Id) + (:(:IdLnk  E)  Id)))
==  oaxioms:EOrderAxioms{i}(E;
==  oaxioms:EOpred?;
==  oaxioms:EOinfo)
==  T:(IdIdType{i})
==  when:(x:Ide:ET(loc(info;e),x))
==  after:(x:Ide:ET(loc(info;e),x))
==  saxiom:(e:E.
==  saxiom:((first(pred?;e)))  (x:Id. when(x,e) = after(x,pred(pred?;e))  T(loc(info;e),x)))
==  V:(KndIdType{i})
==  (val:(e:EV(kind(info;e),loc(info;e)))
==  Top)) 

latex

Definitions	EqDecider(T), Unit, left + right, IdLnk, EOrderAxioms(E; pred?; info), P  Q, A, b, first(e), x:A. B(x), s = t, pred(e), Knd, Id, Type, x:A  B(x), x:AB(x), f(a), kind(e), loc(e), Top
FDL editor aliases	EVal